﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

using TruthTree2.FOL.Logic;

namespace TruthTree2.FOL.Resolution
{
    public class Literal : IComparable<Literal>
    {
        internal bool negated;
        internal AtomicWFF atom;

        public Literal(AtomicWFF a, bool n)
        {
            atom = a;
            negated = n;
        }

        public Literal Rename(Dictionary<Term, Term> b)
        {
            AtomicWFF ren = atom;
            foreach (KeyValuePair<Term, Term> kvp in b)
            {
                ren = (AtomicWFF)ren.Rename(kvp.Key, kvp.Value);
            }

            return new Literal(ren, negated);
        }

        public bool IsNegation(Literal l)
        {
            if (!atom.Equals(l.atom)) { return false; }

            return negated != l.negated;
        }

        public bool IsSamePredicate(Literal l)
        {
            if (atom is Predicate && l.atom is Predicate)
            {
                Predicate a = (Predicate)atom;
                Predicate b = (Predicate)l.atom;

                return a.arity == b.arity && a.name.Equals(b.name);
            }
            else if (atom is Identity && l.atom is Identity) { return true; }

            return false;
        }

        public bool IsSamePredicateNegated(Literal l)
        {
            if (negated == l.negated) { return false; }
            return IsSamePredicate(l);
        }

        public bool Unify(Literal l, out Dictionary<Term, Term> binding)
        {
            binding = new Dictionary<Term, Term>();

            if (atom is Identity || l.atom is Identity)
            {
                Identity i = (Identity)(atom is Identity ? atom : l.atom);
                if (i.left is Constant && !(i.right is Constant))
                {
                    binding[i.right] = i.left;
                }
                else if (i.right is Constant && !(i.left is Constant))
                {
                    binding[i.left] = i.right;
                }
                else
                {
                    binding[i.left] = i.right;
                    binding[i.right] = i.left;
                }

                return true;
            }

            if (!IsSamePredicate(l)) { return false; }

            List<Term> ta = atom.GetTermsInOrder();
            List<Term> tb = l.atom.GetTermsInOrder();

            if (ta.Count != tb.Count) { return false; }

            for (int a = 0; a < ta.Count; a++)
            {
                if (binding.ContainsKey(ta[a])) { binding.Clear(); return false; }

                if (ta[a] is Constant && tb[a] is Constant)
                {
                    if (!ta[a].Equals(tb[a])) { binding.Clear(); return false; }
                }

                binding[ta[a]] = tb[a];
            }

            return true;
        }

        public int CompareTo(Literal l)
        {
            return ToString().CompareTo(l.ToString());
        }

        public override bool Equals(object obj)
        {
            if (obj is Literal)
            {
                Literal l = (Literal)obj;

                if (!atom.Equals(l.atom)) { return false; }

                return negated == l.negated;
            }

            return false;
        }

        public override string ToString()
        {
            return String.Format("{0}{1}",
                (negated ? "¬" : ""),
                atom);
        }

        public override int GetHashCode()
        {
            return ToString().GetHashCode();
        }
    }
}
